f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
↳ QTRS
↳ DependencyPairsProof
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
F(0, 1, g(x, y), z) → F(g(x, y), g(x, y), g(x, y), h(x))
H(g(x, y)) → H(x)
F(0, 1, g(x, y), z) → H(x)
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(0, 1, g(x, y), z) → F(g(x, y), g(x, y), g(x, y), h(x))
H(g(x, y)) → H(x)
F(0, 1, g(x, y), z) → H(x)
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
H(g(x, y)) → H(x)
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(g(x, y)) → H(x)
The value of delta used in the strict ordering is 1/2.
POL(g(x1, x2)) = 1/4 + (7/2)x_1
POL(H(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
F(0, 1, g(x, y), z) → F(g(x, y), g(x, y), g(x, y), h(x))
f(0, 1, g(x, y), z) → f(g(x, y), g(x, y), g(x, y), h(x))
g(0, 1) → 0
g(0, 1) → 1
h(g(x, y)) → h(x)